package mac5789.sat;

import java.io.IOException;
import java.io.InputStream;
import java.util.Iterator;

/**
 * Estreve um problema no formato DIMACS.
 * 
 * @author lundberg
 * 
 */
public class SatProblemInput extends InputStream {

    private final Iterator<Integer[]> clauses;

    private String buffer;

    private int pos = 0;

    /**
     * Construtor
     * 
     * @param problem
     *            problem
     */
    public SatProblemInput(SatProblem problem) {
        this.buffer = String.format("p %s %s %s", problem.getFormat(), problem.getNVariables(), problem.getNClauses());
        this.clauses = problem.getClauses();
    }

    /**
     * {@inheritDoc}
     */
    @Override
    public int read() throws IOException {
        if (this.pos < this.buffer.length()) {
            return this.buffer.charAt(this.pos++);
        } else if (this.clauses.hasNext()) {
            this.buffer = this.nextClause();
            this.pos = 1;
            return this.buffer.charAt(0);
        } else {
            return -1;
        }
    }

    /**
     * 
     * @return next clause
     */
    private String nextClause() {
        StringBuilder builder = new StringBuilder();
        for (Integer literal : this.clauses.next()) {
            builder.append(" " + literal);
        }
        builder.append(" 0");
        return builder.toString();
    }
}
